$\forall$${\it loc}$:Id, $T$:Type, $x$:Id, $v$:$T$. @${\it loc}$ $x$ initially $v$:$T$ $\in$ Realizer